$\forall$$x$:Knd, $T$:Type. normal{-}type\{i:l\}($T$) $\Rightarrow$ normal{-}da\{i:l\}(fpf{-}single($x$; $T$))